package typesys;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import flowlogic.STSimplifier;

import ast.AtomicLabel;
import ast.ChannelConstant;
import ast.DQCSystem;
import ast.Label;
import ast.Principal;
import ast.Procedure;
import ast.Term;
import ast.Process;

public class SystemJudgement extends TypeJudgement {
	
	private DQCSystem system;
	private HashMap<String, HashSet<Term>> rho;
	private HashMap<String, Procedure> procedureMap;
	
	public SystemJudgement(
			DQCSystem system,
			HashMap<String, HashSet<Term>> rho,
			PrincipalHierarchy hierarchy)
	{
		this.system = system;
		this.rho = rho;
		procedureMap = STSimplifier.getProcedureMap();
		setHierarchy(hierarchy);
	}
	
	public boolean check() throws FunctionUndefinedException
	{
		boolean result = true;
		
		Principal o = TopPrincipal.getInstance();
		ArrayList<Term> list = new ArrayList<Term>();
		list.add(TopPrincipal.getInstance());
		AtomicLabel botLabel = new AtomicLabel(o, list); 
		
		HashMap<String, Label> gamma1 = new HashMap<String, Label>();
		for (String cstName : STSimplifier.getChannelMap().keySet()) {
			gamma1.put(cstName, STSimplifier.getChannelMap().get(cstName).getLabel());
		}
				
		for (String procName : procedureMap.keySet()) {
			Procedure curProcedure =  procedureMap.get(procName);
			Process body = curProcedure.getProcess();
			ProcessJudgement pjdgt = new ProcessJudgement(
					body, 
					curProcedure.getBeginLabel(), 
					rho, curProcedure.getSite(), 
					gamma1, 
					getHierarchy());
			
			if (!pjdgt.check()) {
				result = false;
				break;
			}
		}
		
		if (result)
		{
			NetworkJudgement netjdgt = new NetworkJudgement(
					system.getNetwork(), botLabel, rho, gamma1, getHierarchy());
			if (!netjdgt.check())
				result = false;
		}
		
		return result;
	}
}
